(set-logic BV)

(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))

(synth-fun f ( (x (BitVec 64))) (BitVec 64)
(

(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
                    (shl1 Start)
 		    (shr1 Start)
		    (shr4 Start)
		    (shr16 Start)
		    (bvand Start Start)
		    (bvor Start Start)
		    (bvxor Start Start)
		    (bvadd Start Start)
		    (if0 Start Start Start)
 ))
)
)
(constraint (= (f #xB011331E5FD06FA0) #xFFFFF4FEECCE1A02))
(constraint (= (f #x65E9013D54965F34) #xFFFFF9A16FEC2AB6))
(constraint (= (f #x9F8A53553E7CCD80) #xFFFFF6075ACAAC18))
(constraint (= (f #x754428FE70B8541C) #xFFFFF8ABBD7018F4))
(constraint (= (f #x796E25A770C08126) #xFFFFF8691DA588F3))
(constraint (= (f #x0000FFFFFFFFFFFE) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #x09221743EDBB7E3D) #x0000000000000002))
(constraint (= (f #x9E464F22F9514ADF) #x0000000000000002))
(constraint (= (f #xD23B046761535AEF) #x0000000000000002))
(constraint (= (f #x112DED50C2D9FFF7) #x0000000000000002))
(constraint (= (f #x249ECAD65BE222B5) #x0000000000000002))
(constraint (= (f #x394201278433A521) #xFFFFFC6BDFED87BC))
(constraint (= (f #x14094266C1E16013) #xFFFFFEBF6BD993E1))
(constraint (= (f #x128B69559AC02901) #xFFFFFED7496AA653))
(constraint (= (f #x12212251C9BD1255) #xFFFFFEDDEDDAE364))
(constraint (= (f #xA001A644BC842223) #xFFFFF5FFE59BB437))
(check-synth)
